es:ES, i:Id, P:(discrete state@i).
@i stable state.P(state)  
 e@i. P((discrete state when e))  e'e.P((discrete state after e')) 

latex

Definitions

x:A  B(x), ES, Atom$n, Id, x:AB(x), f(a), x(s), t.1, E, s = t, {T}, WellFnd{i}(A;x,y.R(x;y)), (e <loc e'), e loc e' , x:A. B(x), t  T, b, Void, P  Q, False, A, x,y. t(x;y), left + right, P  Q, P & Q, P  Q, P  Q, x. t(x), let x,y = A in B(x;y), loc(e), <a, b>, e@i. P(e), @i stable state.P(state)  , True, (e < e'), T, discrete state@i, (discrete state after e), , x.A(x), (discrete state when e), Type, e'e.P(e'), A c B, pred(e), SQType(T), s ~ t, first(e), {x:A| B(x)}

Lemmas

not wf, assert wf, es-first wf, dstate-after-pred, Id sq, es-pred wf, es-pred-locl, es-le-iff, es-stable wf, es-loc wf, es-dstate-when wf, es-locl-wellfnd, es-locl wf, es-le wf, es-E wf, es-dstate-after wf, es-dstate wf, squash wf, true wf, Id wf, event system wf, es-le-loc, es-loc-pred, all functionality wrt iff, implies functionality wrt iff, wellfounded functionality wrt iff, es-locl-iff